﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Xml;

using System.Diagnostics.Contracts;
using HeapModel.ProgInfo;

namespace HeapModel.ConcreteMemory
{
	/// <summary>
	/// This class represents the store and thus access into the concrete heap model.
	/// This is exported from the runtime traversal during the sampling and then used in the visualization process.
	/// </summary>
	public sealed class ConcreteHeap
	{
		/// <summary>
		/// Tuple of a root name and true if it is a static root, along with the target node
		/// </summary>
		private readonly Dictionary<Tuple<string, bool>, ConcreteNode> m_roots;
		private readonly List<ConcreteNode> m_allnodes;
		private readonly ConcreteNode m_nulltarget;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_roots != null);
			Contract.Invariant(this.m_allnodes != null);
			Contract.Invariant(this.m_nulltarget != null);
		}

		/// <summary>
		/// Allocate an initial empty concrete memory object.
		/// </summary>
		public ConcreteHeap()
		{
			this.m_roots = new Dictionary<Tuple<string, bool>, ConcreteNode>();
			this.m_allnodes = new List<ConcreteNode>();

			this.m_nulltarget = new ConcreteNode(0, new TypeIdentifier("null", TypeIdentifier.TypeCategory.Null), 0, 0);
			this.m_nulltarget.FinalizeTargetSet(new List<ConcretePointer>());
			this.m_allnodes.Add(this.m_nulltarget);
		}

		/// <summary>
		/// Add a new root identifier and associated target (null if the underlying target is null).
		/// </summary>
		public void AddSingleRootTarget(string sn, bool isstackroot, ConcreteNode nn)
		{
			Contract.Requires(sn != null);

			this.m_roots.Add(new Tuple<string, bool>(sn, !isstackroot), nn != null ? nn : this.m_nulltarget);
		}

		/// <summary>
		/// Add a new object to the concrete memory.
		/// </summary>
		public void AddNewObject(ConcreteNode obj)
		{
			Contract.Requires(obj != null);

			this.m_allnodes.Add(obj);
		}

		/// <summary>
		/// Serialize the memory.
		/// </summary>
		public void XMLify(XmlWriter xmlw, List<TypeIdentifier> alltypes, List<OffsetIdentifier> alloffsets)
		{
			Contract.Requires(xmlw != null);

			xmlw.WriteStartElement("ConcreteMemory");

			xmlw.WriteStartElement("TypesUsed");
			foreach(TypeIdentifier outtty in alltypes)
				outtty.SerializeTypeName(xmlw);
			xmlw.WriteEndElement();

			xmlw.WriteStartElement("OffsetsUsed");
			foreach(OffsetIdentifier rrn in alloffsets)
				rrn.SerializeOffsetIdentifier(xmlw);
			xmlw.WriteEndElement();

			xmlw.WriteStartElement("MemoryNodes");
			foreach(ConcreteNode cnode in this.m_allnodes)
			{
				if(!cnode.ConcreteNodeType.IsSpecialNullType)
					cnode.SerializeConcNodeWithOutRefs(xmlw);
			}
			xmlw.WriteEndElement();

			xmlw.WriteStartElement("Pointers");
			foreach(ConcreteNode cnode in this.m_allnodes)
				cnode.SerializeNodePtrs(xmlw);
			xmlw.WriteEndElement();

			xmlw.WriteStartElement("Roots");
			foreach(KeyValuePair<Tuple<String, bool>, ConcreteNode> ucr in this.m_roots)
			{
				xmlw.WriteStartElement("Root");
				xmlw.WriteAttributeString("Name", ucr.Key.Item1);
				xmlw.WriteAttributeString("IsStatic", ucr.Key.Item2.ToString());
				xmlw.WriteAttributeString("Target", ucr.Value.ConcreteNodeID.ToString());
				xmlw.WriteEndElement();
			}
			xmlw.WriteEndElement();
			
			xmlw.WriteEndElement();
		}

		/// <summary>
		/// Deserialize the memory.
		/// </summary>
		public static ConcreteHeap ReadConcreteMemory(XmlReader rr, Dictionary<String, TypeIdentifier> tymap, Dictionary<String, OffsetIdentifier> offsetmap)
		{
			Contract.Requires(rr != null);
			Contract.Requires(tymap != null);
			Contract.Requires(offsetmap != null);
			
			List<TypeParseInfo> typproc = new List<TypeParseInfo>();
			Dictionary<int, ConcreteNode> nmap = new Dictionary<int, ConcreteNode>();
			Dictionary<String, AccessPath> accpdict = new Dictionary<String, AccessPath>();

			rr.ReadStartElement("ConcreteMemory");

			if(rr.IsEmptyElement)
				rr.ReadStartElement("TypesUsed");
			else
			{
				rr.ReadStartElement("TypesUsed");
				while(rr.IsStartElement("TypeDef"))
				{
					TypeParseInfo ttypl = TypeIdentifier.ReadTypeNameDef(rr, tymap);
					typproc.Add(ttypl);
				}
				rr.ReadEndElement();
			}

			if(rr.IsEmptyElement)
				rr.ReadStartElement("OffsetsUsed");
			else
			{
				rr.ReadStartElement("OffsetsUsed");
				while(rr.IsStartElement("OffsetIdentifier"))
				{
					OffsetIdentifier rrn = OffsetIdentifier.ReadOffsetIdentifier(rr, tymap);
					if(!offsetmap.ContainsKey(rrn.NameValue))
						offsetmap.Add(rrn.NameValue, rrn);
				}
				rr.ReadEndElement();
			}

			foreach(TypeParseInfo tyup in typproc)
			{
				foreach(String vpfid in tyup.Item2)
				{
					if(offsetmap.ContainsKey(vpfid))
					{
						OffsetIdentifier vpmfidval = offsetmap[vpfid];
						if(!tyup.Item1.AllOffsetIdentifiers.Contains(vpmfidval))
							tyup.Item1.AllOffsetIdentifiers.Add(vpmfidval);
					}
				}
			}

			ConcreteHeap cmem = new ConcreteHeap();
			nmap.Add(0, cmem.m_allnodes[0]);

			if(rr.IsEmptyElement)
				rr.ReadStartElement("MemoryNodes");
			else
			{
				rr.ReadStartElement("MemoryNodes");
				while(rr.IsStartElement("Node"))
				{
					ConcreteNode obj = ConcreteNode.ReadConcreteNode(rr, tymap);
					nmap.Add(obj.ConcreteNodeID, obj);
					cmem.m_allnodes.Add(obj);
				}
				rr.ReadEndElement();
			}

			int sorttokenctr = 1;

			if(rr.IsEmptyElement)
				rr.ReadStartElement("Pointers");
			else
			{
				rr.ReadStartElement("Pointers");
				while(rr.IsStartElement("ORefs"))
				{
					String idstr = rr.GetAttribute("ID");
					int oid = idstr.StartsWith("0x") ? Int32.Parse(idstr.Substring(2), System.Globalization.NumberStyles.AllowHexSpecifier) : Int32.Parse(idstr);
					ConcreteNode cnode = nmap[oid];
					cnode.ReadConcreteNodeRefsInto(rr, accpdict, offsetmap, nmap, ref sorttokenctr);
				}
				rr.ReadEndElement();
			}

			if(rr.IsEmptyElement)
				rr.ReadStartElement("Roots");
			else
			{
				rr.ReadStartElement("Roots");
				while(rr.IsStartElement("Root"))
				{
					String rname = rr.GetAttribute("Name");
					bool isstatic = Boolean.Parse(rr.GetAttribute("IsStatic"));
					String trgtstr = rr.GetAttribute("Target");
					int target = trgtstr.StartsWith("0x") ? Int32.Parse(trgtstr.Substring(2), System.Globalization.NumberStyles.AllowHexSpecifier) : Int32.Parse(trgtstr);
					ConcreteNode tnode = nmap[target];

					rr.ReadStartElement("Root");

					cmem.m_roots.Add(new Tuple<String, bool>(rname, isstatic), tnode);
				}
				rr.ReadEndElement();
			}

			rr.ReadEndElement();

			return cmem;
		}

		public Dictionary<Tuple<String, bool>, ConcreteNode> Roots
		{
			get 
			{
				Contract.Ensures(Contract.Result<Dictionary<Tuple<String, bool>, ConcreteNode>>() != null);

				return this.m_roots; 
			}
		}

		public ConcreteNode NullTarget
		{
			get
			{
				Contract.Ensures(Contract.Result<ConcreteNode>() != null);

				return this.m_nulltarget;
			}
		}

		public List<ConcreteNode> AllObjects
		{
			get 
			{
				Contract.Ensures(Contract.Result<List<ConcreteNode>>() != null);

				return this.m_allnodes; 
			}
		}
	}
}


